FDL - Nuprl Lemma : do-apply-p-filter

Nuprl Lemma : do-apply-p-filter

T:Type, P:(T

), f:(

x:T. Dec(P(x))), x:T.
(

can-apply(p-filter(f);x))

(do-apply(p-filter(f);x) = x)

Definitions b, do-apply(f;x), p-filter(f), can-apply(f;x), x:AB(x), s = t, P Q, x:A. B(x), t T, f(a), x(s), Dec(P), , Type, False, True, left + right, P Q

Lemmas true wf, false wf, decidable wf